package server.sat;

import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
import java.util.Scanner;

import server.core.Solution;

/**
 * The SATSolution class defines the implementation of the {@link Solution}
 * interface for SAT.
 * 
 * @author Clayton Edward Taylor
 */
public class SATSolution implements Solution {
	
	private final BitSet variables;
	private final int numVars;
	
	/**
	 * Creates a new SATSolution object containing the given solution data.
	 * 
	 * @param data - The solution data as text
	 * @see          SATSolution
	 */
	public SATSolution(String data) {
		
		Scanner parser = new Scanner(data);
		List<Boolean> varList = new ArrayList<Boolean>();
		parser.skip("s (UN)?SATISFIABLE\n(v)?");
		while (parser.hasNext()) {
			int var = parser.nextInt();
			if (var != 0) {
				varList.add(var > 0);
			}
		}
		parser.close();
		this.numVars = varList.size();
		this.variables = new BitSet(numVars);
		for (int i = 0; i < numVars; ++i) {
			variables.set(i, varList.get(i));
		}
	}
	
	/**
	 * Creates a new SATSolution object containing the given solution data and
	 * number of variables.
	 * 
	 * @param numVars - The number of variables
	 * @param data    - The solution data as bits
	 * @see             SATSolution
	 */
	public SATSolution(int numVars, byte[] data) {
		
		this.numVars = numVars;
		this.variables = new BitSet(numVars);
		for (int i = 0; i < numVars; ++i) {
			if ((data[i / 8] & (1 << (i % 8))) > 0) {
				variables.set(i);
			}
		}
	}

	/**
	 * Produces a String representing the data of this SATSolution.
	 * 
	 * @return A String representing the SATSolution
	 * @see    SATSolution
	 */
	@Override
	public String toString() {
		
		if (numVars == 0) {
			return "s UNSATISFIABLE\n";
		}
		StringBuilder sb = new StringBuilder("s SATISFIABLE\nv ");
		for (int i = 0; i < numVars; ++i) {
			if (!variables.get(i)) {
				sb.append("-");
			}
			sb.append(i + 1);
			sb.append(" ");
		}
		sb.append("0\n");
		return sb.toString();
	}
	
	/**
	 * Returns the byte array representation of the solution data.
	 * 
	 * @return The solution data as bits
	 * @see    SATSolution
	 */
	public byte[] getBytes() {
		
		int length = (numVars + 7) / 8;
		byte[] bytes = new byte[length];
		for (int i = 0; i < numVars; ++i) {
			if (variables.get(i)) {
				bytes[bytes.length-i/8-1] |= 1<<(i%8);
			}
		}
		return bytes;
	}
	
	/**
	 * Returns the number of variables in the solution.
	 * 
	 * @return The number of variables
	 * @see    SATSolution
	 */
	public int getNumVariables() {
		
		return numVars;
	}
}
